T:Type, as:(T List), f,g:(T).
subtype_rel(T; )
 sorted(as)
 ((priority-select(f; g; as) = (inl ff )  (?))
  l_exists(as; T; a.(((g(a)))  (b:T. (b  as)  (b  a)  (((f(b)))))))) 

latex

Definitions

x:A  B(x), P  Q, x:A. B(x), sorted(L), l_exists(L; T; x.P(x)), x:AB(x), x:A. B(x), int_seg(i; j), b, void, P  Q, False, A, Type, type List, P  Q, s = t, t  T, l[i], f(a), prop{i:l}, (x  l), a < b, x. t(x), A  B, P  Q, ff, inl x , priority-select(f; g; as), Unit, , left + right, #$n, n + m, ||as||, x.A(x), , lelt(i; j; k), {x:A| B(x)} , decision, subtype(S; T), , grp_car(g), P  Q, decidable(P), divides(b; a), assoced(a; b), set_leq(p; a; b), set_lt(p; a; b), grp_lt(g; a; b), A c B, x f y, l_all(L; T; x.P(x)), ge(i; j), sq_type(T), guard(T)

Lemmas

decidable int equal, decidable le, member wf, select member, subtype rel wf, sorted wf, priority-select-property, iff functionality wrt iff, iff wf, rev implies wf, bool wf, priority-select wf, unit wf, bfalse wf, length wf1, le wf, l member wf, l exists wf, not wf, select wf, assert wf, int seg wf